Inference at * 1 0 
Iof proof for Lemma Agatha Murder Puzzle (JProver)Lori2R:


1. Agatha hates Charles
2. Agatha hates Agatha
3. p:Person. p is richer than Agatha  The Butler hates p
4. p:Person. Agatha hates p  Charles hates p
5. p:Person. Agatha hates p  The Butler hates p
6. p:Person. p hates Agatha  p hates The Butler  p hates Charles
7. p, q:Person. p kills q  p is richer than q
8. p, q:Person. p kills q  p hates q
  The Butler kills Agatha & Charles kills Agatha 

latex

 by allL (3) The Butler 

latex

 1: 
 1: 9. The Butler is richer than Agatha  The Butler hates The Butler
 1:   The Butler kills Agatha & Charles kills Agatha
 .

Definitions

x:AB(x), x:A. B(x), t  T